Termination Proof Script
Consider the TRS R consisting of the rewrite rules
1:
(x
+
y)
+
z
→ x
+
(y
+
z)
2:
f
(x)
+
f
(y)
→
f
(x
+
y)
3:
f
(x)
+
(
f
(y)
+
z)
→
f
(x
+
y)
+
z
There are 5 dependency pairs:
4:
(x
+
y)
+#
z
→ x
+#
(y
+
z)
5:
(x
+
y)
+#
z
→ y
+#
z
6:
f
(x)
+#
f
(y)
→ x
+#
y
7:
f
(x)
+#
(
f
(y)
+
z)
→
f
(x
+
y)
+#
z
8:
f
(x)
+#
(
f
(y)
+
z)
→ x
+#
y
Consider the SCC {4-8}.
The constraints could not be solved.
Tyrolean Termination Tool
(0.02 seconds) --- May 4, 2006